import checkers.oigj.quals.*;

@OI class Node<E> {
    public E value;
    public @OI Node<E> next;
    public @OI Node<E> immNext;
    public Node(E value) { this.value = value; }
    public Node() { }
}

@OI class LinkedList<E> {
    public @PrivateI Node<E> head; // to test make it public
    public @Immutable Node<E> immHead;
    public @OMutable Node<E> mutHead;
    public void test() {
	@PrivateI Node<E> oTemp = head.next;
	head.next = new @PrivateI Node<E>();
	@Immutable Node<E> temp = immHead.immNext;
	mutHead.next = new @OMutable Node<E>();

	head.next = new Node<E>(); // ERROR: should be new @PrivateI Node<E>() instead
	head.next = new @OI Node<E>(); // ERROR: should be new @PrivateI Node<E>() instead
	head.next = new @PublicI Node<E>(); // ERROR: should be new @PrivateI Node<E>()
	@OI Node<E> n = head.next; // ERROR: head.next should be owned by @PrivateI
    }

    
    public @OI Node<E> oHead;
    public @PublicI Node<E> worldHead;
	
    public void testFieldAccessandAsssignment(@PrivateI Node<E> thisE,
					      @OI Node<E> oE,
					      @PublicI Node<E> worldE, 
					      @PrivateI LinkedList<E> thisL,
					      @OI LinkedList<E> oL,
					      @PublicI LinkedList<E> worldL) @OI {
	head = thisE; 
	head = oE; // ERROR: head is @PrivateI
	head = worldE; // ERROR: head is @PublicI
	
	oHead = thisE; // ERROR: oHead is @OI
	oHead = oE; 
	oHead = worldE; // ERROR: head is @OI

	worldHead = thisE; // ERROR: head is @PublicI
	worldHead = oE; // ERROR: head is @PublicI
	worldHead = worldE; 
	
	@PrivateI Node<E> thisE2 = head.next.next;
	@OI Node<E> oE2 = oHead.next.next;
	@PublicI Node<E> worldE2 = worldHead.next.next;
		
	thisE2.next.next = thisE.next;
	oE2.next.next = oE.next;
	worldE2.next.next = worldE.next;
		
	oE2.next.next = thisE.next; // ERROR: different owner annotations
	worldE2.next.next = oE.next; // ERROR: different owner annotations
	thisE2.next.next = worldE.next; // ERROR: different owner annotations

	// testing other LinkedList's
	// Field access
	thisE = this.head; 
	thisE = thisL.head; // ERROR: head is @PrivateI and is only accessible by "this."
	thisE = worldL.head; // ERROR: head is @PrivateI and is only accessible by "this."
	
	oE = this.oHead;
	thisE = thisL.oHead;
	oE = thisL.oHead; // ERROR: thisL.oHead is @PrivateI
	worldE = worldL.oHead; 
	oE = worldL.oHead; // ERROR: worldL.oHead is @PublicI

	worldE = this.worldHead;
	worldE = thisL.worldHead;
	worldE = worldL.worldHead;	
	
	// Field assignment
	this.head = thisE;
	thisL.head = thisE; // ERROR: head is @PrivateI and is only accessible by "this."
	// FIXME: For some reason the following raises count by 2 errors.
	worldL.head = thisE; // ERROR: head is @PrivateI and is only accessible by "this."
	
	this.oHead = oE;
	thisL.oHead = thisE;
	thisL.oHead = oE; // ERROR: thisL.oHead is @PrivateI
	worldL.oHead = worldE;
	worldL.oHead = oE; // ERROR: worldL.oHead is @PublicI
	
	this.worldHead = worldE;
	thisL.worldHead = worldE;
	worldL.worldHead = worldE;	
    }

    public void testMethodInvocation(@PrivateI Node<E> thisE,
				     @OI Node<E> oE,
				     @PublicI Node<E> worldE, 
				     @PrivateI LinkedList<E> thisL,
				     @OI LinkedList<E> oL,
				     @PublicI LinkedList<E> worldL) @OI {
	// method return is like field access
	thisE = this.getPrivateIHead(); 
	thisE = thisL.getPrivateIHead(); // ERROR: head is @PrivateI accessible by "this"
	thisE = worldL.getPrivateIHead(); // ERROR: head is @PrivateI accessible by "this"
	
	oE = this.getOHead();
	thisE = thisL.getOHead();
	oE = thisL.getOHead(); // ERROR: thisL.getOHead() is @PrivateI
	worldE = worldL.getOHead(); 
	oE = worldL.getOHead(); // ERROR: worldL.getOHead() is @PublicI

	worldE = this.getPublicIHead();
	worldE = thisL.getPublicIHead();
	worldE = worldL.getPublicIHead();	
		
	// method arguments is like field assignment		
	this.setPrivateIHead(thisE);
	thisL.setPrivateIHead(thisE); // ERROR: head is @PrivateI only accessible by "this"
	worldL.setPrivateIHead(thisE); // ERROR: head is @PrivateI only accessible by "this"
		
	this.setOHead(oE);
	thisL.setOHead(thisE);
	thisL.setOHead(oE); // ERROR: thisL.setOHead is @PrivateI
	worldL.setOHead(worldE);
	worldL.setOHead(oE); // ERROR: worldL.setOHead is @PublicI
	
	this.setPublicIHead(worldE);
	thisL.setPublicIHead(worldE);
	worldL.setPublicIHead(worldE);
    }
    public @PrivateI Node<E> getPrivateIHead() @OI { return head; }
    public @OI Node<E> getOHead() @OI { return oHead; }
    public @PublicI Node<E> getPublicIHead() @OI { return worldHead; }
    
    public void setPrivateIHead(@PrivateI Node<E> h) @OI { head = h; }
    public void setOHead(@OI Node<E> h) @OI { oHead = h; }
    public void setPublicIHead(@PublicI Node<E> h) @OI { worldHead = h; }	

    /*
    public void testOwnerShipNesting() {
	@PrivateI LinkedList<@PrivateI Data> l1;
	@PublicI LinkedList<@PublicI Data> l2;
	@PrivateI LinkedList<@PublicI Data> l3;
	@PublicI LinkedList<@PrivateI Data> l4; // ERROR: ownership nesting violated
	@OI LinkedList<@PrivateI Data> l5; // ERROR or do we constrain O to always be Private ?
	@OI LinkedList<@PublicI Data> l6;
	@OI LinkedList<@OI Data> l7;
	@PublicI LinkedList<@OI Data> l8; // ERROR or do we constrain O to always be Public ?
	@PrivateI LinkedList<@OI Data> l9;
    }
	// testing generic method parameter and ownership
	// like:  <O2 extends Private, I2 extends ReadOnly> void testGeneric(Node<O2,I2,E> n) {...}
	public @OI("2") void testGenericPrivate(@OI("2") Node<E> n) {
		@OI("2") LinkedList<@PrivateI Node<E>> l;
	}
	public @OI("2") void testGenericPublic(@OI("2") Node<E> n) {
		@PublicI LinkedList<@OI("2") Node<E>> l;
	}
	public void testCallGeneric() {
		testGenericPrivate(head);
		testGenericPrivate(oHead); // ERROR or do we constrain O to always be Private ?
		testGenericPrivate(worldHead); // ERROR: ownership nesting violated
		testGenericPrivate(head); // ERROR: ownership nesting violated
		testGenericPrivate(oHead); // ERROR or do we constrain O to always be Public ?
		testGenericPrivate(worldHead); 
	}
    */
}

@OI class Data {
    public @OI String value;
    public Data(String value) { this.value = value; }
}

@OI class OIGJExample {
    public static void main(String[] args) {
	@OMutable Data d1 = new @OMutable Data("Data 1");
	Node<@OMutable Data> n1 = new Node<@OMutable Data>(d1);
	LinkedList<@OMutable Data> ll1 = new LinkedList<Data>();
	// FIXME: For some reason the following raises count by 2 errors.
	ll1.head = n1; // ERROR: ll1.head is owned by @PrivateI only accessible by "this."
    }
}
